\begin{tabbing}
R{-}Feasible(\=ecl{-}machine at "b" with state ecl\+
\\[0ex]
\\[0ex]eclseq(eclbase(rcv(lnk1\{a to b\},"x");$\lambda$$s$,$v$.
\\[0ex]$s$("x")$<_{2}$$v$).1;eclbase(rcv(lnk1\{a to b\},"y");$\lambda$$s$,$v$. $v$$<_{2}$$s$("x")).2)
\\[0ex]
\\[0ex]state variables "x" : $\mathbb{Z}$
\\[0ex]
\\[0ex]actions \=rcv(lnk1\{a to b\},"x") : $\mathbb{Z}$ $\oplus$ rcv(lnk1\{a to b\},"y") : $\mathbb{Z}$ $\oplus$ \+
\\[0ex]rcv(lnk1\{b to output\},"hello") : $\mathbb{B}$
\\[0ex]
\-\\[0ex]sends r\=cv(lnk1\{a to b\},"y") sends on lnk1\{b to output\}\+
\\[0ex]with tag "hello" [$s$,$v$.true$_{2}$], at marker 2
\\[0ex]
\-\\[0ex]updates \=update{-}spec1(rcv(lnk1\{a to b\},"x");"x";1;$s$,$v$.$v$) $\oplus$ \+
\\[0ex]update{-}spec1(rcv(lnk1\{a to b\},"y");"x";2;$s$,$v$.$v$)
\-\-\\[0ex]$\oplus$ @"a" \=precondition for "a"(v:Unit):\+
\\[0ex]$\lambda$$s$,$v$. $s$("x")$<$10 State("x" : $\mathbb{Z}$) v
\-\\[0ex]$\oplus$ @"a" effect locl("a")(v:Unit)  "x" := $\lambda$$s$,$v$. $s$("x")+1 State("x" : $\mathbb{Z}$) v 
\\[0ex]$\oplus$ \=sends locl("a")(v:Unit) on lnk1\{a to b\}:\+
\\[0ex]tagged([$\langle$"x"$,\,$$\lambda$$s$,$v$. [$s$("x")]$\rangle$],State("x" : $\mathbb{Z}$),v):"x" : $\mathbb{Z}$
\-\\[0ex]$\oplus$ \=sends rcv(lnk1\{input to a\},"key")(v:$\mathbb{Z}$) on lnk1\{a to b\}:\+
\\[0ex]tagged([$\langle$"y"$,\,$$\lambda$$s$,$v$. [$v$]$\rangle$],State(),v):"y" : $\mathbb{Z}$
\-\\[0ex]$\oplus$ \=sends rcv(lnk1\{input to a\},"string")(v:Atom) on lnk1\{a to b\}:\+
\\[0ex]tagged([$\langle$"string"$,\,$$\lambda$$s$,$v$. [$v$]$\rangle$],State(),v):"string" : Atom
\-\\[0ex]$\oplus$ \=sends rcv(lnk1\{input to a\},"b")(v:$\mathbb{B}$) on lnk1\{a to b\}:\+
\\[0ex]tagged([$\langle$"b"$,\,$$\lambda$$s$,$v$. [$v$]$\rangle$],State(),v):"b" : $\mathbb{B}$
\-\\[0ex]$\oplus$ \=sends rcv(lnk1\{input to a\},"hello")(v:Unit) on lnk1\{a to b\}:\+
\\[0ex]tagged([$\langle$"hello"$,\,$$\lambda$$s$,$v$. [$v$]$\rangle$],State(),v):"hello" : Unit)
\-
\end{tabbing}